PRISM

./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 cluster.prism cluster.props --property below_min -const N=64,T=2000,t=20

PRISM
=====

Version: 4.5.dev
Date: Sat Mar 14 13:56:04 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 cluster.prism cluster.props --property below_min -const 'N=64,T=2000,t=20'

Parsing model file "cluster.prism"...

Type:        CTMC
Modules:     Left Right Repairman Line ToLeft ToRight 
Variables:   left_n left right_n right r line line_n toleft toleft_n toright toright_n 

Parsing properties file "cluster.props"...

8 properties:
(1) "below_min": R{"time_not_min"}=? [ C<=T ]
(2) "operational": R{"percent_op"}=? [ I=t ]
(3) "premium_steady": S=? [ "premium" ]
(4) "qos1": P=? [ F<=T !"minimum" ]
(5) "qos2": P=? [ F[t,t] !"minimum" ]
(6) "qos3": P=? [ "minimum" U<=t "premium" ]
(7) "qos4": P=? [ !"minimum" U>=t "minimum" ]
(8) "repairs": R{"num_repairs"}=? [ C<=T ]

---------------------------------------------------------------------

Model checking: "below_min": R{"time_not_min"}=? [ C<=T ]
Model constants: N=64
Property constants: T=2000

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...
Model constants: N=64

Computing reachable states...

Reachability (BFS): 133 iterations in 0.14 seconds (average 0.001053, setup 0.00)

Time for model construction: 0.1 seconds.

Type:        CTMC
States:      151060 (1 initial)
Transitions: 733216

Rate matrix: 8225 nodes (71 terminal), 733216 minterms, vars: 23r/23c

Computing rewards...
Engine: Sparse

Building sparse matrix... [n=151060, nnz=733216, compact] [2.9 MB]
Creating vector for diagonals... [dist=3049, compact] [318.9 KB]
Allocating iteration vectors... [3 x 1.2 MB]
TOTAL: [6.7 MB]

Uniformisation: q.t = 51.257040 x 2000.000000 = 102514.080000
Fox-Glynn: left = 100270, right = 105233

Starting iterations...
Iteration 1215 (of 105233): max relative diff=0.009761, 5.00 sec so far
Iteration 2426 (of 105233): max relative diff=0.004201, 10.00 sec so far
Iteration 3637 (of 105233): max relative diff=0.003186, 15.01 sec so far
Iteration 4849 (of 105233): max relative diff=0.002502, 20.01 sec so far
Iteration 6055 (of 105233): max relative diff=0.002244, 25.01 sec so far
Iteration 7266 (of 105233): max relative diff=0.001665, 30.01 sec so far
Iteration 8477 (of 105233): max relative diff=0.000338, 35.02 sec so far
Iteration 9687 (of 105233): max relative diff=0.000026, 40.02 sec so far
Iteration 10898 (of 105233): max relative diff=0.000002, 45.02 sec so far

Steady state detected at iteration 12101

Iterative method: 12101 iterations in 50.64 seconds (average 0.004131, setup 0.66)

Value in the initial state: 0.004219443769591423

Time for model checking: 50.499 seconds.

Result: 0.004219443769591423 (value in the initial state)


Overall running time: 51.19 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.